Formal verification techniques have been playing an important role inpre-silicon validation processes. One of the most important points consideredin performing formal verification is to define good verification scopes; weshould define clearly what to be verified formally upon designs under tests. Weconsidered the following three practical requirements when we defined the scopeof formal verification. They are (a) hard to verify (b) small to handle, and(c) easy to understand. Our novel approach is to break down generic propertiesfor system into stereotype properties in block level and to define requirementsfor Verifiable RTL. Consequently, each designer instead of verification expertscan describe properties of the design easily, and formal model checking can beapplied systematically and thoroughly to all the leaf modules. During thedevelopment of a component chip for server platforms, we focused on RAS(Reliability, Availability, and Serviceability) features and described morethan 2000 properties in PSL. As a result of the formal verification, we foundseveral critical logic bugs in a short time with limited resources, andsuccessfully verified all of them. This paper presents a study of thefunctional verification methodology.
展开▼
